$\forall$$A$:Type, $B$:($A$$\rightarrow$Type), $p$:($x$:$A$$\times$$B$($x$)), $C$:Type, $b$:($x$:$A$$\rightarrow$$B$($x$)$\rightarrow$$C$).
\\[0ex]($p$/$x$,$y$. $b$($x$,$y$)) $=$ $b$(1of($p$),2of($p$))